refactor: golf proofs#1364
Open
Vilin97 wants to merge 33 commits into
Open
Conversation
Contributor
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
Golf proof bodies in Space/Norm/Basic and Space/IsDistBounded: term-mode collapses, Tendsto composition in place of manual rpow juggling, and anonymous-constructor witnesses. Statements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Golf proof bodies in WickContraction/InsertAndContractNat and Sign/InsertSome: reuse erase_insert and getDualErase lemmas, replace manual Fin.succAbove case bashes with omega fed the relevant order couplings. Statements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Golf proof bodies in Electromagnetism/Dynamics/KineticTerm and QuantumMechanics SpectralTheory/Basic. Statements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…oofs Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…y, speed-unit proofs Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…-field proofs Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…e proofs Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…ce proofs Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…l, rigid-body proofs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…al-ensemble proofs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Vilin97
force-pushed
the
claude/golf-proofs-more
branch
from
7fe99cd to
587a2c7
Compare
…e, EM potential proofs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
…st, tensor-constructor proofs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Vilin97
force-pushed
the
claude/golf-proofs-more
branch
from
1fe17b6 to
456a04a
Compare
Vilin97
added a commit
to Vilin97/physlib
that referenced
this pull request
Jul 6, 2026
Move the remaining Mistral golf from leanprover-community#1364 to leanprover-community#1373: simplify isTotalTimeDerivative_neg, totalTimeDerivative_contDiff, and totalTimeDerivative_hasVarGradientAt_equivalence. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai> Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Vilin97
added a commit
to Vilin97/physlib
that referenced
this pull request
Jul 6, 2026
Move the remaining Mistral golf from leanprover-community#1364 to leanprover-community#1373: simplify isTotalTimeDerivative_neg, totalTimeDerivative_contDiff, and totalTimeDerivative_hasVarGradientAt_equivalence. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai> Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace non-terminal broad simp calls with Lean-generated simp only sets and split the long DimSevenPlane simp line reported by the Python style linter. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Contributor
Author
|
/check-golf |
Contributor
🏌️ check-golf reportComparing base Result: ✅ Statements preserved. Every changed declaration kept its statement; only proofs / bodies changed.
Of the golfed proofs/bodies above, the trivial reshapes were:
🔧 Definition bodies changed (data may have changed, type unchanged) (2)The defining term outside
✅ Proofs golfed (1503)
✅ Embedded proofs golfed (type unchanged) (1)
✅ Definition proofs golfed (data unchanged) (9)
⏱️ Compile cost (base → head)Measured 124 file(s) with body changes (1 could not be measured in isolation).
Largest heartbeat changes (122 of 124 files differ)
Generated by |
Contributor
Author
|
/check-golf |
Member
|
@Vilin97 Hmm doesn't seem like that check-golf updated the comment. |
jstoobysmith
reviewed
Jul 8, 2026
jstoobysmith
left a comment
jstoobysmith
left a comment
Member
There was a problem hiding this comment.
Picked out first instance of something novel
| simpa [hωa] using S.ω_sq | ||
| field_simp [S.m_ne_zero] at hωsq | ||
| nlinarith | ||
| rw [S.k_eq_m_mul_ω_sq, S.isCriticallyDamped_decayRate hS] |
| rw [hforce] | ||
| simp [inner_smul_right] | ||
| linear_combination (norm := module) h1 t | ||
| simp [hforce, inner_smul_right] |
| linarith | ||
| rw [IsCriticallyDamped, discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS | ||
| have hsq : S.decayRate ^ 2 = S.ω ^ 2 := by nlinarith [sq_pos_of_pos S.m_pos] | ||
| nlinarith [S.decayRate_nonneg, S.ω_pos] |
| rw [Time.deriv_eq, fderiv_const_mul (by fun_prop), _root_.smul_apply, | ||
| fderiv_inner_apply (𝕜 := ℝ) hd hd, ← Time.deriv_eq] | ||
| simp [inner_smul_right, real_inner_comm] | ||
| ring |
| · exact contDiff_const | ||
| · exact ContDiff.inner (𝕜 := ℝ) (contDiff_fst.comp contDiff_snd) | ||
| (contDiff_fst.comp contDiff_snd) | ||
| fun_prop |
| ring | ||
| rw [h2] | ||
| exact tendsto_const_nhds.mul (tendsto_const_nhds.mul (tendsto_const_nhds.mul | ||
| ((normPowerSeries_tendsto x hx).zpow₀ _ (.inl (norm_ne_zero_iff.mpr hx))))) |
| exact distDiv_inv_pow_eq_dim (d := d) | ||
| rw [hdiv] | ||
| rw [smul_smul] | ||
| rw [hdist, map_smul, distDiv_inv_pow_eq_dim, smul_smul] |
| rw [integral_congr_ae (ae_of_all _ fun i => 𝓒.log_physicalProbability T i), | ||
| integral_add h_int_log_prob (integrable_const _), integral_const] | ||
| simp only [probReal_univ, smul_eq_mul] | ||
| ring |
| rw [differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ 𝓒 T hE, | ||
| helmholtzFreeEnergy_def, log_partitionFunction, kB_mul_beta T hT] | ||
| field_simp | ||
| ring |
| simp [scaleUnit] | ||
| simp [TemperatureUnit.div_eq_val, toReal] | ||
| simp [dimScale, scaleUnit] | ||
| simp [LengthUnit.div_eq_val, TimeUnit.div_eq_val, MassUnit.div_eq_val, ChargeUnit.div_eq_val, |
Contributor
Author
|
/check-golf |
Vilin97
changed the title
The measure-path file selection referenced a nonexistent FileReport attribute, crashing every /check-golf run since leanprover-community#1356. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
|
/check-golf |
Vilin97
force-pushed
the
claude/golf-proofs-more
branch
2 times, most recently
from
d2f4d05 to
85379c2
Compare
The /check-golf compile-cost report flagged 6 files where golfing increased elaboration cost (total +346k heartbeats, worst 7x). Re-golf or revert the offending proofs so every file is now at or below its pre-golf heartbeat count, keeping the rest of the golf: InsertAndContractNat 198,524 -> 27,386 (base 27,760) Sign/InsertSome 150,267 -> 72,575 (base 75,708) StaticContract 74,661 -> 38,487 (base 39,702) ComplexTensor/Basic 319,007 -> 268,044 (base 288,579) Wirtinger/Basic 72,201 -> 50,708 (base 54,086) DimSevenPlane 103,363 -> 84,498 (base 85,591) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Contributor
Author
|
/check-golf |
Member
|
The change in heartbeats Also merge conflict :). |
…more Conflict in ComplexTensor/Weyl/Two.lean resolved by taking master's version: leanprover-community#1407 renamed the Weyl basis identifiers, so this branch's golfed proofs there no longer apply.
Contributor
Author
|
good to merge once you are happy with it |
Member
There was a problem hiding this comment.
This file again. Maybe we should add .pyc to the gitignore
Member
There was a problem hiding this comment.
But also need to delete it here
Member
There was a problem hiding this comment.
Still needs deleting from here :)
- CKMMatrix/Basic: the nine phase-shift component lemmas now use squeezed simp only [...] sets instead of broad simp (review: 'a bit bad as not simp only'). - Grad: replace the rw-with-hypothesis ending of distGrad_eq_sum_basis by a direct (distGrad_inner_eq ..).trans h1.symm term (review: 'odd'). - Remove scripts/__pycache__/check_golf.cpython-312.pyc that entered via the leanprover-community#1400 merge. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Golfs proofs across Physlib: streamlining arguments, using stronger mathlib lemmas and tactics, removing redundant steps, and increasing code reuse. No statements or definitions are changed — only proofs.
Rebased directly onto
master(previously stacked on the now-closed #1332; all of that PR's golfs were dropped — this diff is exclusively this PR's own work).Stats (final)
-Dwarn.sorry=false -Dweak.says.verify=true; fulllake buildgreen (9,121 jobs) at the final tip; a signature audit over every changed file confirms all declaration headers (statements) are byte-identical to master.Process disclosure (per AI-POLICY.md)
claude-fable-5) and Claude Opus 4.8 (claude-opus-4-8). One max-reasoning subagent per file, each self-verifying via a per-filelake env leancompile with the CI flags, followed by an independent re-verification, statement-safety diff scan, and a full workspace build before each push.Prompt used
🤖 Generated with Claude Code
https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3